\r\n\tA set is naturally used to collect distinct elements sharing some property.\r\n\tCombinatorial search problems over these data structures can thus be naturally\r\n\tmodelled by high level languages with set abstraction facilities, and efficiently\r\n\tsolved if constraint reasoning prunes search space when the sets are not fully\r\n\tknown a priori (i.e. they are variables ranging over a set domain).\r\n\t
\r\n\tMany complex relations between sets can be expressed with constraints such as set\r\n\tinclusion, disjointness and equality over set expressions that may include such\r\n\toperators as intersection, union or difference of sets. Also, as it is often the\r\n\tcase, one is not interested simply on these relations but on some attribute or\r\n\tfunction of one or more sets (e.g. the cardinality of a set). For instance, the\r\n\tgoal of many problems is to maximise or minimise the cardinality of a set. Even\r\n\tfor satisfaction problems, some sets, although still variables, may be constrained\r\n\tto a fixed cardinality or a stricter cardinality domain than just the one inferred\r\n\tby the domain of a set variable (for instance, the cardinality of a set may have\r\n\tto be restricted to be an even number).\r\n\t
\r\n\tCardinal represents set variables by set intervals with a lower and an upper bound\r\n\tconsidering set inclusion as a partial ordering. Consistency techniques are then\r\n\tapplied to set constraints by interval reasoning. A set domain variable S may be\r\n\tspecified by an interval [A,B] where A and B are known sets ordered by set inclusion,\r\n\trepresenting the greatest lower bound and the lowest upper bound of S, respectively.\r\n\t
\r\n\tThe cardinality of a set S, given as a finite domain variable C (#S=C), is not a\r\n\tbijective function since two distinct sets may have the same cardinality. Still,\r\n\tit can be constrained by the cardinalities of the set bounds.\r\n\t
\r\n\tA simple inference that can be done using cardinality information is to instantiate\r\n\tthe set to one of the set bounds, when it is known that the set cardinality must be\r\n\tequal to the cardinality of that bound. But Cardinal does much more than that.\r\n\tFor instance, consider two set variables\r\n\tS1,S2, that can assume either set value {} (empty set) or {a,b}. Their set domain\r\n\tis thus [{},{a,b}] with cardinality 0 or 2. The intersection of S1 and S2 also\r\n\tyelds set domain [{},{a,b}]. But we need a special inference to conclude that the\r\n\tintersection cardinality is also either 0 or 2 (it can not be 1). Set solvers\r\n\tother than Cardinal do not make such inferences.\r\n\t
\r\n\tInferences using cardinalities can be very useful to deduce more rapidly the\r\n\tnon-satisfiability of a set of constraints, thus improving efficiency of\r\n\tcombinatorial search problem solving. As another simple example, if Z is known to be\r\n\tthe set difference between Y and X, both contained in set {a,b,c,d}, and it is known\r\n\tthat X has exactly 2 elements, it should be inferred that the cardinality of Z can\r\n\tnever exceed 2 elements (i.e. from X,Y in {a,b,c,d}, #X=2, Z=Y\\X it should be\r\n\tinferred that #Z =< 2). A failure could thus be immediately detected upon the\r\n\tposting of a constraint such as #Z=3.\r\n\t
\r\n\tInference capabilities such as these are particularly important when solving set\r\n\tproblems where cardinality plays a special role. Cardinal thus fully uses\r\n\tconstraint propagation on sets cardinality.\r\n\t
\r\n\r\nIntervals and Lattices\r\n\t
\r\n\tSet intervals define a lattice of sets. The set inclusion relation between two\r\n\tsets defines a partial order on P(U), the powerset over a certain universe U,\r\n\tthe set of all subsets of U.\r\n\t
\r\n\tDue to the transitivity rule, the top set, U, includes all sets of P(U);\r\n\twhile the bottom set, {}, is included in all sets of P(U). Consequently,\r\n\tsets U and {} constitute an upper bound and a lower bound of P(U), respectively.\r\n\tIn addition, they are the least upper bound (lub) or join, and the greatest lower\r\n\tbound (glb) or meet of P(U), since there is no other upper bound contained in\r\n\t(\221less\222 than) U nor other lower bound containing (\221greater\222 than) the empty set {}.\r\n\t
\r\n\tLet us now consider for U={a,b,c,d}, the sub-lattice connecting {a,b,d} and {b}\r\n\t(thus also including sets {a,b} and {b,d}). Sets {} and {a,b,c,d} are still a\r\n\tlower and an upper bound, but this time the glb is {b} and the lub is {a,b,d}.\r\n\t
\r\n\tThe two bounds (glb and lub) define a set interval (e.g. [{b},{a,b,d}]) and may\r\n\tform the domain of a set variable S, meaning that set S is one of those defined\r\n\tby its interval (lattice); all other sets outside this domain are excluded from\r\n\tthe solution. Thus, b is definitely an element of S, while a and d are the only\r\n\tother possible elements.\r\n\t
\r\n\tSet interval reasoning allows us to apply consistency techniques such as Bounded\r\n\tArc Consistency, due to the monotonic property of set inclusion.\r\n\t
\r\n\tAny set variable must then have a domain consisting of a set interval. In addition,\r\n\tthis interval should be kept as small as possible, in order to discard all sets\r\n\tthat are known not to belong to the solution, while not loosing any of the still\r\n\tpossible values (sets). The smallest such domain is the one with equal glb and lub,\r\n\ti.e. a domain of the form [B,B], corresponding to a constant set B. For a set\r\n\tvariable that can assume any set value from a collection of known sets, such as\r\n\t{{a,b},{a,c},{d}}, the corresponding interval is the convex closure of such\r\n\tcollection (which in this case is the set interval [{},{a,b,c,d}]). In general,\r\n\tfor n possible arbitrary sets S1...Sn, the corresponding set variable X has an\r\n\tinterval domain [glb, lub] where glb is the intersection of all S1...Sn, and lub\r\n\tis their union.\r\n\t
\r\nImplementation Notes\r\n\t
\r\n\tIn Cardinal, all sets are represented as sorted lists, which eases working with\r\n\tsets and lists interchangeably.\r\n\t
\r\n\tSet variable bounds are represented by its glb and its lub\\glb, the set of\r\n\tadditional possible elements, which we refer to as poss.\r\n\t
\r\n\tCardinal implements a number of set constraints such as inclusion, equality,\r\n\tinequality, membership, disjointness, and even complement, together with set\r\n\toperations (union, intersection and difference), as built-in.\r\n\t
\r\n\tAs mentioned, Cardinal also allows the definition and use of optional set functions\r\n\t(other than cardinality): minimum and maximum, for sets of integers, and union,\r\n\tfor sets of sets. Refer to the available predicates for details.\r\n")). :- comment(struct(cardinal), [summary : "Cardinal attributes of a set variable", fields : [domain : "Set domain in the form [Glb:NIn,Poss:NMax], where Glb is the set's\r\n\t\t\tglb, NIn its cardinality, Poss is its poss (i.e. its lub\\glb),\r\n\t\t\tand NMax is the lub's cardinality (i.e. NIn + #(Poss)).\r\n\t\t\tIf it is a set of sets and a union function attribute has been\r\n\t\t\tdeclared, then each element of Poss comes annotated with its\r\n\t\t\trespective length.", cardinality : "Cardinality function (an integer or an FD variable).", minimum : "Minimum function (an integer or an FD variable),\r\n\t\t\tfor sets of integers. Free variable if unused.", maximum : "Maximum function (an integer or an FD variable),\r\n\t\t\tfor sets of integers. Free variable if unused.", union : html("Union function, for sets of sets. Free variable if unused;\r\n\t\t\totherwise, a list in the form\r\n\t\t\t[UnionVar, GlbU+PossU, Singles, Lengths], where:
\r\nUnionVar: A set (variable or ground) corresponding to the union of the set's elements\r\n\t(sets themselves);\r\nGlbU: Set union of the set's glb;\r\nPossU: Set of possible union elements with counters (X:N), i.e. an ordered\r\n\tlist of all elements in the sets in set's poss (lub\\glb)\r\n\twith the number of occurrences attached\r\nSingles: Set of elements where N=1 in PossU"), bounded : "Suspension list.", glb : "Suspension list.", lub : "Suspension list.", bound : "Suspension list."]]). :- comment(# / 2, [amode : #(?, ?), args : ["SetExpression" : "A Set expression.", "Cardinality" : "An integer or an FD variable."], summary : "Cardinality of a set expression", desc : html("Cardinality is the cardinality of SetExpression, a set term possibly\r\n\t\tincluding set operators `/\\, `\\/ and `\\ (or \\).
\r\n\t\tSetExpression is first evaluated into a ground set or a set variable and then\r\n\t\tits Cardinality is applied as in cardinality/2."), resat : "No.", fail_if : "Fails if Cardinality can not be the cardinality of SetExpression.", eg : "\r\n?- S `::[]..[a,b], #(S,C).\r\n?- S `::[]..[a,b], #(S `/\\ [b,c],1).\r\n?- S `::[]..[a,b], #([b,c] `\\/ S `\\ [a,z] `/\\ [g], C).\r\nC = 2,\r\n?- S `::[]..[a,b], #(([b,c] `\\/ S `\\ [a,z]) `/\\ [g], C).\r\nC = 0\r\n?- S1 `::[]..[a,b], S2 `::[]..[b,c,d], #(S1 `/\\ S2, 2).\r\nno\r\n", see_also : [cardinality / 2, `= / 2]]). :- comment(`$ / 2, [template : "?SetVar1 `$ ?SetVar2", args : ["SetVar1" : "A set variable.", "SetVar2" : "A set variable."], summary : "Set disjointness constraint", desc : html("Constrain sets SetVar1 and SetVar2 to be disjoint. I.e. SetVar1 and\r\n\t\tSetVar2 should have no common elements (empty intersection)."), resat : "No.", fail_if : "Fails if SetVar1 and SetVar2 can not be disjoint.", eg : "\r\n?- [] `$ [8], [7] `$ [8], [] `$ [].\r\nyes\r\n\r\n?- [7,8] `$ [8] ; [7] `$ [7,8] ; [a] `$ [a] ; [a,b] `$ [b,a].\r\nno\r\n\r\n?- sets([X,Y], [],[8,9], [cardinality:1]), X `$ Y, set_labeling([X,Y]).\r\nX = [8], Y = [9] ;\r\nX = [9], Y = [8] ;\r\nno\r\n\r\n?- S `:: []+[a,b], X=S, X `$ S.\r\nS = [], X = []\r\n\r\n?- sets([X,Y], [],[7,8,9], [cardinality:2]), X `$ Y.\r\nno\r\n\r\n?- sets([X,Y], [],[7,8,9], [cardinality:[1,2]]), X `$ Y, #(X,2), #(Y,C).\r\nC = 1\r\n\r\n?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], X `$ Y, c `@ Y, poss(X,PX), poss(Y,PY).\r\nPX = [b,d], PY = [b,d,e,f]\r\n", see_also : [all_disjoint / 1, `<> / 2, complement / 2, complement / 3, `/= / 2, `>= / 2]]). :- comment(`-@ / 2, [template : "?Element `-@ ?SetVariable", args : ["SetVariable" : "A set variable.", "Element" : "A ground term or a variable."], summary : "Set non-membership constraint", desc : html("Constrain SetVariable to not include Element.
\r\n\t\tIf Element is a variable then the constraint\r\n\t\tis suspended until it becomes ground."), resat : "No.", fail_if : "Fails if Element must be a member of SetVariable.", eg : "\r\n?- S `:: []..[a,b], a `-@ S, glb_poss(S,G,P).\r\nG = [], P = [b]\r\n\r\n?- S `:: [c]+[a,b], c `-@ S.\r\nno\r\n\r\n?- S `:: [a]+[b,c], z `-@ S, glb_poss(S,G,P).\r\nG = [a], P = [b,c]\r\n\r\n?- S `:: []..[a,b], X `-@ S, glb_poss(S,G,P).\r\nG = [], P = [a,b]\r\n\r\n?- S `:: []..[a,b], X `-@ S, X=b, glb_poss(S,G,P).\r\nG = [], P = [a]\r\n", see_also : [`@ / 2, in / 2, notin / 2, `:: / 2]]). :- comment(`/= / 2, [template : "?SetVar1 `/= ?SetVar2", args : ["SetVar1" : "A set variable.", "SetVar2" : "A set variable."], summary : "Set inequality constraint", desc : html("Constrain sets SetVar1 and SetVar2 to be different.
\r\n\t\tThis constraint is suspended until one of the two sets is bound\r\n\t\tto another set (variable or ground)."), resat : "No.", fail_if : "Fails if SetVar1 and SetVar2 must be the same set.", eg : "\r\n?- [] `/= [8], [7] `/= [8], [7,8] `/= [8], [7] `/= [7,8].\r\nyes\r\n\r\n?- [] `/= [] ; [a] `/= [a] ; [a,b] `/= [b,a].\r\nno\r\n\r\n?- sets([X,Y], [],[8,9], [cardinality:1]), X `/= Y, set_labeling([X,Y]).\r\nX = [8], Y = [9] ;\r\nX = [9], Y = [8] ;\r\nno\r\n\r\n?- sets([X,Y], [],[8,9], []), X `/= Y, X=Y.\r\nno\r\n\r\n?- X `:: [8]+[8,9], [8,9] `/= X, card_labeling([X]).\r\nX = [8] ;\r\nno\r\n", see_also : [`$ / 2, complement / 2, complement / 3, `= / 2]]). :- comment(`:: / 2, [template : "?SetVariable `:: ?Domain", args : ["SetVariable" : "A variable.", "Domain" : "A set domain with optional cardinality declaration."], summary : "Set variable declaration", desc : html("Declare or constrain a set domain variable to have Domain as domain.
\r\n\t\tDomain may assume 3 forms: Glb..Lub, Glb+Poss or Glb+Poss:Cardinality.
\r\n\t\tGlb is a ground set denoting the SetVariable's glb. Lub is a ground set\r\n\t\tdenoting the SetVariable's lub. Poss is a ground set denoting the SetVariable's\r\n\t\tposs (lub\\glb). Cardinality is the SetVariable's cardinality, which may be\r\n\t\tan integer, an FD variable, or an integer domain (list or range)."), resat : "No.", fail_if : "Fails if SetVariable can not be constrained accordingly.", eg : "\r\n?- S `:: []..[a,b].\r\n?- S `:: []+[a,b].\r\n?- S `:: []+[a,b]:1.\r\n?- S `:: [x]+[a,b]:C.\r\n?- S `:: []+[a,b]:[0,2].\r\n?- S `:: [c]+[a,b,d,e,f,g,h,i,j,k]:[2,4..7].\r\n", see_also : [set / 4, sets / 4, cardinality / 2, union_var / 2, minimum / 2, maximum / 2, set_labeling / 1]]). :- comment(`< / 2, [template : "?SetVar1 `< ?SetVar2", args : ["SetVar1" : "A set variable.", "SetVar2" : "A variable."], summary : "Set inclusion constraint (obsolete)", desc : html("Constrain sets SetVar1 and SetVar2 so that SetVar2 contains SetVar1.
\r\n\t\tObsolete: (`<)/2 is available only for compatibility with conjunto library syntax.\r\n\t\tIt is equivalent (with swapped arguments) to the preferred `>=/2.\r\n\t\tSee its description for details."), see_also : [`>= / 2, `= / 2]]). :- comment(`<> / 2, [template : "?SetVar1 `<> ?SetVar2", args : ["SetVar1" : "A set variable.", "SetVar2" : "A set variable."], summary : "Set disjointness constraint (obsolete)", desc : html("Constrain sets SetVar1 and SetVar2 to be disjoint.
\r\n\t\tObsolete: `<>/2 is available only for compatibility with conjunto library syntax.\r\n\t\tIt is equivalent to the preferred `$/2. See its description for details."), see_also : [`$ / 2, all_disjoint / 1, complement / 2, complement / 3, `/= / 2, `>= / 2]]). :- comment(`= / 2, [template : "?SetExp1 `= ?SetExp2", args : ["SetExp1" : "A set expression.", "SetExp2" : "A set expression."], summary : "Set equality constraint", desc : html("Constrain sets in both hand sides of equation so that SetExp1 and\r\n\t\tSetExp2 represent the same set.
\r\n\t\tA set expression is a set (variable or ground) or a set operation between\r\n\t\ttwo set expressions. Possible set operations are set union, set intersection\r\n\t\tand set difference, and the respective operators are `\\/, `/\\ and `\\.\r\n\t\tThese operators are defined as:\r\n
\r\n:- op(500, yfx, `\\/). %set union\r\n:- op(400, yfx, `/\\). %set intersection\r\n:- op(300, yfx, `\\ ). %set difference\r\n"), resat : "No.", fail_if : "Fails if SetExp1 can not be the same set as SetExp2.", eg : "\r\n/*\r\nExamples of equalities between set expressions, being S,T,U,V,W,X,Y,Z set variables:\r\n\r\nX `= Y\r\nS `\\/ Y `\\ Z `= T `/\\ S `\\/ U `/\\ W\r\nV `\\ ([a,b,d] `\\/ W) `\\/ (S `\\ W) `= ((T `/\\ [3,9]) `\\/ W) `\\ U\r\n*/\r\n\r\n% just union:\r\n?- [8,a,9] `\\/ [i,8,o] `\\/ [] `\\/ [a,8,5] `= U.\r\nU = [5,8,9,a,i,o]\r\n\r\n?- X `\\/ Y `= [8,9], glb_poss(X,GX,PX), glb_poss(Y,GY,PY).\r\nGX = [], PX = [8,9], GY = [], PY = [8,9]\r\n\r\n?- X `:: [a]+[b,c], X `\\/ [b,n] `= U, glb_poss(X,GX,PX), glb_poss(U,GU,PU).\r\nGX = [a], PX = [b,c], GU = [a,b,n], PU = [c]\r\n\r\n?- sets([A,B],[a,b],[d,g,h,j],[cardinality:4]), A`\\/B`=U, #(U,C), fd:dom(C,DomC).\r\nDomC = [4,5,6]\r\n\r\n?- sets([X,Y],[a,b],[d,g,h,j],[]), X`\\/Y`=U, #(U,4), #(Y,C), fd:dom(C,DomC).\r\nDomC = [2,3,4]\r\n\r\n?- sets([S,X], [],[a,b], [cardinality:[0,2]]), U `= X `\\/ S, #(U,C), fd:dom(C,DomC).\r\nDomC = [0,2]\r\n\r\n?- S `:: [a,c]+[b,g,h,j,l]:3, X`::[a]+[b,h,t,u,y]:2, U `= X `\\/ S, #(U,C), fd:dom(C,DomC).\r\nDomC = [3,4]\r\n\r\n?- S `:: [a,c]+[b,g,h,j,l], X`::[a]+[b,h,t,u,y], U `= X `\\/ S, #(U,C), fd:(C::0..3), #(X,CX), fd:dom(CX,DomCX).\r\nDomCX = [1,2]\r\n\r\n\r\n% just intersection:\r\n?- I `= [4,6] `/\\ [3,6,8].\r\nI = [6]\r\n\r\n?- [a,b,c,d,e] `/\\ [a,b,c,e,f,g] `/\\ [b,d,e,f,x,y] `= I.\r\nI = [b,e]\r\n\r\n?- X `:: [a]+[b,c], X `/\\ [b,n] `= I, glb_poss(X,GX,PX), glb_poss(I,GI,PI).\r\nGX = [a], PX = [b,c], GI = [], PI = [b]\r\n\r\n?- S `:: [a]+[b,c], X`::[]+[7,8,9], I`::[]+[a,b,c,7,z,99], I `= X `/\\ S.\r\nI = []\r\n\r\n?- sets([A,B],[a,b],[d,g,h,j],[cardinality:5]), A`/\\B`=I, #(I,C), fd:dom(C,DomC).\r\nDomC = [4,5]\r\n\r\n?- S `:: [a,c]+[g,h,j,l], X`::[a]+[b,h,t,u,y], I `= X `/\\ S, #(I,C), fd:dom(C,DomC).\r\nDomC = [1,2]\r\n\r\n\r\n% just difference:\r\n?- D `= [4,6] `\\ [3,6,8].\r\nD = [4]\r\n\r\n?- [a,b,c,d,e] `\\ [a,e,f,g] `\\ [b,d,e,f,x,y] `= D.\r\nD = [c]\r\n\r\n?- [a,b,c,d,e] `\\ ([a,e,f,g] `\\ [b,d,e,f,x,y]) `= D.\r\nD = [b,c,d,e]\r\n\r\n?- X `:: [a]+[b,c], X `\\ [b,n] `= D, glb_poss(X,GX,PX), glb_poss(D,GD,PD).\r\nGX = [a], PX = [b,c], GD = [a], PD = [c]\r\n\r\n?- S `:: [a]+[b,c], X`::[]+[7,8,9], D`::[]+[a,b,c,7,z,99], D `= X `\\ S, glb_poss(D,GD,PD).\r\nGD = [], PD = [7]\r\n\r\n?- sets([A,B],[a,b],[d,g,h,j],[cardinality:5]), A`\\B`=D, #(D,C), fd:dom(C,DomC).\r\nDomC = [0,1]\r\n\r\n?- sets([X,Y],[a,b],[d,g,h,j],[]), X`\\Y`=D, #(D,4).\r\nX = [a,b,d,g,h,j], Y = [a,b]\r\n\r\n?- S `:: [a,c,z]+[g,h], X`::[a]+[b,c,h,t], D `= S `\\ X, #(D,C), fd:dom(C,DomC).\r\nDomC = [1,2,3,4].\r\n\r\n?- S `:: []+[a,b], X=S, #(S `\\ X, C).\r\nC = 0", see_also : [`/= / 2, set_labeling / 1, set_labeling / 2]]). :- comment(`>= / 2, [template : "?SetVar1 `>= ?SetVar2", args : ["SetVar1" : "A set variable.", "SetVar2" : "A variable."], summary : "Set inclusion constraint", desc : html("Constrain sets SetVar1 and SetVar2 so that SetVar1 contains SetVar2.
\r\n\t\tIf SetVar2 is not yet a set domain variable it is declared as such, using\r\n\t\tSetVar1's lub."), resat : "No.", fail_if : "Fails if SetVar1 can not contain SetVar2.", eg : "\r\n?- [7,8,9] `>= [7,9], [7,8,9] `>= [7,8,9], [7,8,9] `>= [], [7,8,9] `>= [9].\r\nyes\r\n\r\n?- [1,7,9] `>= [7,8].\r\nno\r\n\r\n?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], X `>= Y, poss(Y,PY).\r\nPY = [a,b,c,d]\r\n\r\n?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], Y `>= X, glb(Y,GY).\r\nGY = [a]\r\n\r\n?- X `:: [a]+[b,c,d,z]:CX, Y `:: []+[a,b,c,d,e,f]:CY, X `>= Y, CX=2, fd:maxdomain(CY,MaxCY).\r\nMaxCY = 2\r\n\r\n?- X `:: [a]+[b,c,d,z]:CX, Y `:: []+[a,b,c,d,e,f]:CY, X `>= Y, CY=3, fd:mindomain(CX,MinCX).\r\nMinCX = 3.\r\n", see_also : [`< / 2, `= / 2]]). :- comment(`@ / 2, [template : "?Element `@ ?SetVariable", args : ["SetVariable" : "A set variable.", "Element" : "A ground term or a variable."], summary : "Set membership constraint", desc : html("Constrain SetVariable to include Element.
\r\n\t\tIf Element is a variable then if SetVariable is a ground singleton,\r\n\t\tthen Element is unified with its single element, otherwise the constraint\r\n\t\tis suspended until Element or SetVariable is ground."), resat : "No.", fail_if : "Fails if Element can not be a member of SetVariable.", eg : "\r\n?- S `:: []..[a,b], a `@ S, glb_poss(S,G,P).\r\nG = [a], P = [b]\r\n\r\n?- S `:: []+[a,b], c `@ S.\r\nno\r\n\r\n?- S `:: [a]+[b,c], a `@ S, glb_poss(S,G,P).\r\nG = [a], P = [b,c]\r\n\r\n?- S `:: []..[a,b], X `@ S, glb_poss(S,G,P).\r\nG = [], P = [a,b]\r\n\r\n?- S `:: []..[a,b], X `@ S, X=b, glb_poss(S,G,P).\r\nG = [b], P = [a]\r\n\r\n?- S `:: [a]+[b,c]:C, X `@ S, C=1.\r\nX = a\r\n", see_also : [in / 2, `-@ / 2, notin / 2, `:: / 2]]). :- comment(all_disjoint / 1, [amode : all_disjoint(+), args : ["SetVars" : "A list of set variables."], summary : "All sets disjointness global constraint", desc : html("Constrain all pairs of sets in SetVars to be disjoint. I.e. No two sets\r\n\t\tcan have a common element (empty pairwise intersection).
\r\n\t\tThis version of all_disjoint/1 is a weak global constraint, but stronger\r\n\t\tthan the simple posting of all pairwise disjoint/2 constraints, since\r\n\t\tit posts the additional constraint that the sum of the cardinalities of\r\n\t\tSetVars must be less than or equal to the cardinality of the union of all\r\n\t\tthe initial LUBs."), resat : "No.", fail_if : "Fails if SetVars can not be all disjoint.", eg : "\r\n?- all_disjoint([[7],[8],[i,k]]).\r\nyes\r\n\r\n?- all_disjoint([[7,8],[i],[8]]).\r\nno\r\n\r\n?- sets([X,Y,Z], [],[1,2,7,8,9], [cardinality:2]), all_disjoint([X,Y,Z]).\r\nno\r\n\r\n?- sets([X,Y,Z], [],[1,2,7,8,9], [cardinality:2]), all_disjoint([X,Y,Z]), 2 `@ X, lub(Y,LubY), lub(Z,LubZ)\r\nLubY = [1,7,8,9], LubZ = [1,7,8,9]\r\n", see_also : [`$ / 2, `<> / 2, complement / 2, complement / 3, `/= / 2, `>=, all_union / 2]]). :- comment(all_union / 2, [amode : all_union(+, ?), args : ["SetVars" : "A list of variables.", "Union" : "A variable or a ground set."], summary : "Union constraint of a list of sets", desc : html("Constraint: Union is the set union of SetVars.
\r\n\t\tAny variable in SetVars that is not yet a set domain variable, is declared\r\n\t\tas such using Union's lub."), resat : "No.", fail_if : "Fails if Union can not be the union of SetVars.", eg : "\r\n?- all_union([[8,a,9],[i,8,o],[],[a,8,5]], U).\r\nU = [5,8,9,a,i,o].\r\n\r\n?- all_union([X,Z,S,Y,T], [8,9]), glb_poss(X,GX,PX), glb_poss(Y,GY,PY).\r\nGX = [], PX = [8,9], GY = [], PY = [8,9]\r\n\r\n?- X `:: [a]+[b,c], all_union([X,[b,n],X], U), glb_poss(X,GX,PX), glb_poss(U,GU,PU).\r\nGX = [a], PX = [b,c], GU = [a,b,n], PU = [c]\r\n\r\n?- sets([X,Y,Z],[a,b],[d,g,h,j],[cardinality:4]), all_union([X,Y,Z],U), #(U,C), fd:dom(C,DomC).\r\nDomC = [4,5,6]\r\n\r\n?- sets([X,Y,Z],[a,b],[d,g,h,j],[]), all_union([X,Y,Z],U), #(U,4), #(Y,C), fd:dom(C,DomC).\r\nDomC = [2,3,4]\r\n", see_also : [`= / 2, all_disjoint / 1]]). :- comment(card_labeling / 1, [amode : card_labeling(?), args : ["SetVars" : "A list of set variables."], summary : "Label cardinality of set variables", desc : html("Instantiate all cardinalities of variables in SetVars from first to\r\n\t\tlast, using indomain/1 predicate of fd library.
\r\n\t\tcard_labeling/1 is defined as:\r\n
\r\n card_labeling([]).\r\n card_labeling([H|T]):-\r\n\tcardinality(H, C),\r\n\tindomain(C),\r\n\tcard_labeling(T).\r\n\r\n"), resat : "Yes.", fail_if : "Fails if cardinalities of SetVars can not be labeled (because constraint\r\n\t\tpropagation leads to a failure).", eg : "\r\n?- S `:: [a]+[b,c]:CS, T `:: [1] + [2], card_labeling([S, T]).\r\nCS = 1, S = [a], T = [1] ;\r\nCS = 1, S = [a], T = [1, 2] ;\r\nCS = 2, T = [1] ;\r\nCS = 2, T = [1, 2] ;\r\nCS = 3, S = [a,b,c], T = [1] ;\r\nCS = 3, S = [a,b,c], T = [1, 2] ;\r\nno\r\n\r\n?- S `:: [a] + [b,c,d,e,f]:[2,3,6,9], card_labeling([S]), cardinality(S,C).\r\nC = 2 ;\r\nC = 3 ;\r\nC = 6, S = [a,b,c,d,e,f] ;\r\nno\r\n\r\n", see_also : [set_labeling / 2, refine / 2, cardinality / 2]]). :- comment(cardinality / 2, [amode : cardinality(?, ?), args : ["SetVariable" : "A Set (variable or ground).", "Cardinality" : "An integer or an FD variable."], summary : "Cardinality of a set", desc : html("Cardinality is the cardinality of SetVariable. If Cardinality is given\r\n\t\t(as an integer or FD variable), then SetVariable is constrained to have such cardinality.\r\n\t\tIf Cardinality is a free variable, then it is unified with the set's cardinality as\r\n\t\tan FD variable or an integer (if it is already known)."), resat : "No.", fail_if : "Fails if Cardinality can not be the cardinality of SetVariable.", eg : "\r\n?- S `::[]..[a,b], cardinality(S,C).\r\n?- S `::[]..[a,b], cardinality(S,1).\r\n?- S `::[]+[a,b]:1, cardinality(S,C).\r\nC = 1\r\n\r\n?- cardinality([a,b],C).\r\nC = 2\r\n\r\n?- S `::[c]+[a,b]:[1,3], C #> 1, cardinality(S,C).\r\nS = [a,b,c]\r\nC = 3", see_also : [# / 2]]). :- comment(complement / 2, [amode : complement(?, ?), args : ["SetVar" : "A variable.", "Complement" : "A variable"], summary : "Set complement constraint", desc : html("Constrain sets so that Complement is the complement set of SetVar.\r\n\t\t(The universe is taken as the union of their LUBs.)."), resat : "No.", fail_if : "Fails if Complement can not be the set complement of SetVar (in their universe).", eg : "\r\n?- complement([8,9], []), complement([8,9], [t]).\r\nyes\r\n\r\n?- complement([8,9], [8]).\r\nno\r\n\r\n?- complement([8,9], N).\r\nN = []\r\n\r\n?- sets([X,Y], [],[7,8,9], []), complement(X,Y), 8 `@ Y, glb_poss(X,GX,PX), glb_poss(Y,GY,PY).\r\nGX = [], PX = [7,9], GY = [8], PY = [7,9]\r\n\r\n?- sets([X,Y], [],[7,8,9], [cardinality:C]), complement(X,Y), card_labeling([X]).\r\nno\r\n\r\n?- sets([X,Y], [],[7,8,9], []), complement(X,Y), X `>= Y, set_labeling(up,[Y]).\r\nY = [], X = [7,8,9] ;\r\nno\r\n\r\n?- sets([X,Y], [],[7,8,9], [minimum:Min]), complement(X,Y), refine(up,X).\r\nno\r\n\r\n?- sets([X,Y], [],[7,8,9], []), complement(X,Y), #(X,1), #(Y,CY).\r\nCY = 2\r\n", see_also : [complement / 3, `$ / 2, `= / 2]]). :- comment(complement / 3, [amode : complement(?, ++, ?), args : ["SetVar" : "A variable.", "Universe" : "A ground set.", "Complement" : "A variable"], summary : "Set complement constraint", desc : html("Constrain sets so that Complement is the complement set of SetVar,\r\n\t\twith respect to the given Universe. I.e. Complement is Universe \\ SetVar.
\r\n\t\tIf a variable (SetVar or Complement) is not yet a set domain variable,\r\n\t\tit is declared as such, limited by the Universe.
\r\n\t\tThis constraint is usually more efficient (stronger) than posting an\r\n\t\tequivalent set difference constraint, due to specific inferences."), resat : "No.", fail_if : "Fails if Complement can not be the set complement of SetVar in set universe Universe.", eg : "\r\n?- complement([7,8], [1,7,8,9], N).\r\nN = [1,9]\r\n\r\n?- complement(N, [1,7,8,9], [7,8]).\r\nN = [1,9]\r\n\r\n?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], complement(X, [a,b,c,d,e,f,g], Y).\r\nno\r\n\r\n?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], complement(X,[a,b,f],Y), domain(X,DX),domain(Y,DY).\r\nDX = [[a]:1,[b]:2], DY = [[f]:1,[b]:2]\r\n\r\n?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], complement(X, [a,b,c,d,e,f], Y), domain(Y,DY).\r\nDY = [[e,f]:2,[b,c,d]:5]\r\n", see_also : [complement / 2, `$ / 2, `= / 2]]). :- comment(domain / 2, [amode : domain(?, -), args : ["SetVariable" : "A set variable.", "Domain" : "A list (pair) with glb and poss."], summary : "Accessing the domain of a set", desc : html("Domain is unified with the domain of SetVariable in the form [Glb:NIn,Poss:NMax],\r\n\t\twhere Glb is the (greatest) lower bound of SetVariable, and NIn its length,\r\n\t\tPoss is the set of still possible elements of SetVariable (i.e. its lub\\glb),\r\n\t\tand NMax is the lub's cardinality (i.e. NIn + #(Poss)).
\r\n\t\tIf SetVariable is a set of sets and a union function attribute has been set,\r\n\t\tthen each element of Poss comes annotated with its respective length."), resat : "No.", fail_if : "Fails if Domain can not be unified with the current domain of SetVariable.", eg : "\r\n?- S `::[c]+[a,b], domain(S,D).\r\nD = [[c]:1, [a,b]:3]\r\n\r\n?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c]]), domain(S,D).\r\nD = [[]:0, [[a,b]:2, [a,c]:2, [b]:1, [b,c]:2]:4]\r\n", see_also : [domain / 3, glb / 2, poss / 2, glb_poss / 3, lub / 2, lub / 4]]). :- comment(domain / 3, [amode : domain(?, ?, ?), args : ["SetVariable" : "A set variable.", "Cardinality" : "An FD variable", "Domain" : "A list (pair) with glb and poss."], summary : "Accessing the domain of a set", desc : html("Domain is unified with the domain of SetVariable (which has cardinality\r\n\t\tCardinality) in the form [Glb:NIn,Poss:NMax],\r\n\t\twhere Glb is the (greatest) lower bound of SetVariable, and NIn its length,\r\n\t\tPoss is the set of still possible elements of SetVariable (i.e. its lub\\glb),\r\n\t\tand NMax is the lub's cardinality (i.e. NIn + #(Poss)).\r\n\t\t
\r\n\t\tIf SetVariable is a set of sets and a union function attribute has been set,\r\n\t\tthen each element of Poss comes annotated with its respective length.\r\n\t\t
\r\n\t\tUse domain/3 instead of domain/2 whenever Cardinality variable is available,\r\n\t\tfor efficiency reasons, since in the case of SetVariable being already\r\n\t\tground, it is not neccessary to recalculate its length (to retrieve\r\n\t\t[Setvariable:Cardinality,[]:Cardinality]. This is due to the loss of\r\n\t\tattributes of variables when these become instantiated.\r\n\t\t
\r\n\t\tCardinality should be input to domain/3. Do not use this predicate to\r\n\t\tretrieve the cardinality of a set, for it will only work when set is ground."), resat : "No.", fail_if : "Fails if Domain can not be unified with the current domain of SetVariable.", eg : "\r\n?- S `::[c]+[a,b]:C, domain(S,C,D).\r\nD = [[c]:1, [a,b]:3]\r\n\r\n?- S `::[c]+[a,b]:C, S=[a,c], domain(S,C,D).\r\nD = [[a,c]:2, []:2]\r\n\r\n?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c],cardinality:C]), domain(S,C,D).\r\nD = [[]:0, [[a,b]:2, [a,c]:2, [b]:1, [b,c]:2]:4]\r\n", see_also : [domain / 2, glb / 2, poss / 2, glb_poss / 3, lub / 2, lub / 4, cardinality / 2, # / 2]]). :- comment(glb / 2, [amode : glb(?, -), args : ["SetVariable" : "A set variable.", "Glb" : "A set."], summary : "Obtaining a set's glb", desc : html("Glb is unified with the (greatest) lower bound of SetVariable."), resat : "No.", fail_if : "Fails if Glb can not be unified with the current glb of SetVariable.", eg : "\r\n?- S `::[c]+[a,b], glb(S,G).\r\nG = [c]\r\n", see_also : [glb_poss / 3, domain / 2, domain / 3, lub / 2, lub / 4, poss / 2]]). :- comment(glb_poss / 3, [amode : glb_poss(?, -, -), args : ["SetVariable" : "A set variable.", "Glb" : "A set.", "Poss" : "A set."], summary : "Obtaining both the glb and the still possible elements of a set", desc : html("Glb is unified with the (greatest) lower bound of SetVariable.
\r\n\t\tPoss is unified with the set of still possible elements of SetVariable\r\n\t\t(i.e. its lub\\glb).
\r\n\t\tIf SetVariable is a set of sets and a union function attribute has been set,\r\n\t\tthen each element of Poss comes annotated with its respective length."), resat : "No.", fail_if : "Fails if Glb can not be unified with the current glb of SetVariable or\r\n\t\tif Poss can not be unified with the current poss (lub\\glb) of SetVariable.", eg : "\r\n?- S `::[c]+[a,b], glb_poss(S,G,P).\r\nG = [c]\r\nP = [a,b]\r\n\r\n?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c]]), glb_poss(S,G,P).\r\nG = []\r\nP = [[a, b] : 2, [a, c] : 2, [b] : 1, [b, c] : 2]\r\n", see_also : [glb / 2, poss / 2, domain / 2, domain / 3, lub / 2, lub / 4]]). :- comment(in / 2, [template : "?Element in ?SetVariable", args : ["SetVariable" : "A set variable.", "Element" : "A ground term or a variable."], summary : "Set membership constraint", desc : html("Constrain SetVariable to include Element.
\r\n\t\tin/2 is available for compatibility with conjunto library syntax.\r\n\t\tIt is equivalent to the preferred `@/2. See its description for details."), resat : "No.", fail_if : "Fails if Element can not be a member of SetVariable.", see_also : [`@ / 2, `-@ / 2, notin / 2, `:: / 2]]). :- comment(lub / 2, [amode : lub(?, -), args : ["SetVariable" : "A set variable.", "Lub" : "A set."], summary : "Obtaining a set's lub", desc : html("Lub is unified with the (least) upper bound of SetVariable."), resat : "No.", fail_if : "Fails if Lub can not be unified with the current lub of SetVariable.", eg : "\r\n?- S `::[c]+[a,b], lub(S,L).\r\nL = [a,b,c]\r\n", see_also : [lub / 4, glb / 2, poss / 2, glb_poss / 3, domain / 2, domain / 3]]). :- comment(lub / 4, [amode : lub(?, -, -, -), args : ["SetVariable" : "A set variable.", "Glb" : "A set.", "Poss" : "A set.", "Lub" : "A set."], summary : "Obtaining a set's lub, together with its glb and poss (lub\\glb)", desc : html("Lub is unified with the (least) upper bound of SetVariable.
\r\n\t\tGlb is unified with the (greatest) lower bound of SetVariable.
\r\n\t\tPoss is unified with the set of still possible elements of SetVariable\r\n\t\t(i.e. its lub\\glb).
\r\n\t\tIf SetVariable is a set of sets and a union function attribute has been set,\r\n\t\tthen each element of Poss comes annotated with its respective length."), resat : "No.", fail_if : "Fails if Lub can not be unified with the current lub of SetVariable or\r\n\t\tif Glb can not be unified with the current glb of SetVariable or\r\n\t\tif Poss can not be unified with the current poss (lub\\glb) of SetVariable.", eg : "\r\n?- S `::[c]+[a,b], lub(S,G,P,L).\r\nG = [c]\r\nP = [a,b]\r\nL = [a,b,c]\r\n\r\n?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c]]), lub(S,G,P,L).\r\nG = []\r\nP = [[a, b] : 2, [a, c] : 2, [b] : 1, [b, c] : 2]\r\nL = [[a, b], [a, c], [b], [b, c]]\r\n", see_also : [lub / 2, glb_poss / 3, glb / 2, poss / 2, domain / 2, domain / 3]]). :- comment(maximum / 2, [amode : maximum(?, ?), args : ["SetVariable" : "A Set (variable or ground) of integers.", "Max" : "An integer or an FD variable."], summary : "Maximum of a set of integers", desc : html("Max is the maximum (i.e. the highest element) of SetVariable.
\r\n\t\tIf Max is given (as an integer or FD variable) then SetVariable is\r\n\t\tconstrained to have such maximum.\r\n\t\tIf Max is a free variable, then it is unified with the set's maximum as\r\n\t\tan FD variable or an integer (if it is already known).
\r\n\t\tmaximum/2 can thus be used either to declare (or constrain) a maximum\r\n\t\tfunction or to retrieve it."), resat : "No.", fail_if : "Fails if Max can not be the maximum of SetVariable.", eg : "\r\n?- S`::[]..[1,2], maximum(S,M).\r\n?- set(S,[],[1,2],[maximum:2], maximum(S,M).\r\nM = 2\r\n\r\n?- S`::[]+[1,2], maximum(S,1).\r\nS = [1]\r\n\r\n?- set(S,[],[1,2],[maximum:1], maximum(S,M).\r\nS = [1]\r\nM = 1", see_also : [minimum / 2, set / 4, sets / 4, cardinality / 2]]). :- comment(minimum / 2, [amode : minimum(?, ?), args : ["SetVariable" : "A Set (variable or ground) of integers.", "Min" : "An integer or an FD variable."], summary : "Minimum of a set of integers", desc : html("Min is the minimum (i.e. the lowest element) of SetVariable.
\r\n\t\tIf Min is given (as an integer or FD variable) then SetVariable is\r\n\t\tconstrained to have such minimum.\r\n\t\tIf Min is a free variable, then it is unified with the set's minimum as\r\n\t\tan FD variable or an integer (if it is already known).
\r\n\t\tminimum/2 can thus be used either to declare (or constrain) a minimum\r\n\t\tfunction or to retrieve it."), resat : "No.", fail_if : "Fails if Min can not be the minimum of SetVariable.", eg : "\r\n?- S`::[]..[1,2], minimum(S,M).\r\n?- set(S,[],[1,2],[minimum:1], minimum(S,M).\r\nM = 1\r\n\r\n?- S`::[]+[1,2], minimum(S,2).\r\nS = [2]\r\n\r\n?- set(S,[],[1,2],[minimum:2], minimum(S,M).\r\nS = [2]\r\nM = 2", see_also : [maximum / 2, set / 4, sets / 4, cardinality / 2]]). :- comment(my_print_set_handler / 2, hidden). :- comment(my_unify_sets_handler / 2, hidden). :- comment(notin / 2, [template : "?Element notin ?SetVariable", args : ["SetVariable" : "A set variable.", "Element" : "A ground term or a variable."], summary : "Set non-membership constraint", desc : html("Constrain SetVariable to not include Element.
\r\n\t\tnotin/2 is available for compatibility with conjunto library syntax.\r\n\t\tIt is equivalent to the preferred `-@/2. See its description for details."), resat : "No.", fail_if : "Fails if Element must be a member of SetVariable.", see_also : [`-@ / 2, `@ / 2, in / 2, `:: / 2]]). :- comment(poss / 2, [amode : poss(?, -), args : ["SetVariable" : "A set variable.", "Poss" : "A set."], summary : "Obtaining the still possible elements of a set (lub\\glb)", desc : html("Poss is unified with the set of still possible elements of SetVariable\r\n\t\t(i.e. its lub\\glb).
\r\n\t\tIf SetVariable is a set of sets and a union function attribute has been set,\r\n\t\tthen each element of Poss comes annotated with its respective length."), resat : "No.", fail_if : "Fails if Poss can not be unified with the current poss (lub\\glb) of SetVariable.", eg : "\r\n?- S `::[c]+[a,b], poss(S,P).\r\nP = [a,b]\r\n\r\n?- S `::[[c]]+[[a,b]], poss(S,P).\r\nP = [[a,b]]\r\n\r\n?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c]]), poss(S,P).\r\nP = [[a, b] : 2, [a, c] : 2, [b] : 1, [b, c] : 2]\r\n", see_also : [glb / 2, glb_poss / 3, domain / 2, domain / 3, lub / 2, lub / 4]]). :- comment(refine / 2, [amode : refine(++, ?), args : ["UpDown" : "Atom ('up' or 'down').", "SetVar" : "A set variable."], summary : "Refine a set variable's domain", desc : html("Pick the first element of SetVar's poss (lub\\glb) and try to include it\r\n\t\tin its glb, or to definitely exclude it from the domain.
\r\n\t\tIf heuristic UpDown is 'up' then inclusion is tried first; otherwise (down)\r\n\t\texclusion is tried first."), resat : "Yes.", fail_if : "Fails if Var can not be refined (it is either ground or both the inclusion\r\n\t\tand exclusion of the first element of its poss leads to a failure due to\r\n\t\tunsatisfied constraints).", eg : "\r\n?- S `:: [a]+[b,c], refine(up,S), glb_poss(S,G,P).\r\nG = [a,b], P = [c] ;\r\nG = [a], P = [c] ;\r\nno\r\n\r\n?- S `:: [a]+[b,c], refine(down,S), glb_poss(S,G,P).\r\nG = [a], P = [c] ;\r\nG = [a,b], P = [c] ;\r\nno\r\n", see_also : [set_labeling / 2, set_labeling / 1]]). :- comment(set / 4, [amode : set(?, ++, ++, +), args : ["SetVariable" : "A variable.", "Glb" : "A ground set.", "Poss" : "A ground set.", "Functions" : "A list."], summary : "Set variable declaration with optional functions", desc : html("Declare or constrain a set domain variable to have Glb as assured\r\n\t\telements and Poss as the possible additional elements.
\r\n\t\tFunctions is a list of functions over SetVariable in the form\r\n\t\tFunctionName:FunctionValue, where FunctionName can be 'cardinality',\r\n\t\t'minimum', 'maximum' or 'union':\r\n
\r\n cardinality: FunctionValue can be an integer, an FD variable or an integer domain (list or range)\r\n union: (SetVariable must be a set of sets.) FunctionValue can be a set, a set variable\r\n\tor a set domain in the form GlbUnion+PossUnion, representing the glb and poss of\r\n\tthe union of SetVariable\r\n minimum and maximum: (SetVariable must be a nonempty set of integers.)\r\n\tFunctionValue can be an integer, an FD variable or an integer domain\r\n\r\n\t\tCardinal inferences over SetVariable and its union, minimum and maximum\r\n\t\tfunctions will be performed only if these functions are explicitly\r\n\t\tdeclared, whereas the cardinality function and respective inferences\r\n\t\twill always be present even if this (cardinality) function is not\r\n\t\texplicitly declared. Note that a simple function declaration such as\r\n\t\tminimum:_ is sufficient to make it 'active'."), resat : "No.", fail_if : "Fails if SetVariable can not be constrained accordingly.", eg : "\r\n?- set(S,[],[a,b],[]).\r\n?- set(S,[],[a,b],[cardinality:1]).\r\n?- set(S,[],[a,b],[cardinality:C]).\r\n?- set(S,[],[a,b],[cardinality:[0,2]]).\r\n?- set(S,[c],[a,b,d,e,f,g,h,i,j,k],[cardinality:[2,4..7]]).\r\n?- set(S,[],[1,3,4,5,7],[minimum:Min,maximum:Max]), fd:(Max #> Min+2).\r\n?- set(S, [], [[1,2,5],[2,4],[3,5],[1,3,4]],\r\n\t[cardinality:2, union:[1,2,3,4,5]]). %set-covering\r\n?- set(S, [], [[1,2,5],[2,4],[3,5],[1,3,4]], [union:[1]+[2,4,5]]).\r\n", see_also : [sets / 4, `:: / 2, cardinality / 2, union_var / 2, minimum / 2, maximum / 2, set_labeling / 1]]). :- comment(set_labeling / 1, [amode : set_labeling(?), args : ["SetVars" : "A variable or a list of set variables."], summary : "Label set variable(s)", desc : html("Instantiate all variables in SetVars from first to last, with\r\n\t\tconsecutive refinements of their domains until they are ground.
\r\n\t\tFor each set variable, for each element in its poss (lub\\glb), inclusion\r\n\t\tis tried first.
\r\n\t\tSetVars can be a set variable instead of a list. Labeling a single set\r\n\t\tvariable S can thus be done both with set_labeling([S]) or with\r\n\t\tset_labeling(S)."), resat : "Yes.", fail_if : "Fails if SetVars can not be labeled (there is no solution to the CSP).", eg : "\r\n?- S `:: [a] + [b, c], T `:: [1] + [2], set_labeling([S, T]).\r\nS = [a, b, c], T = [1, 2] ;\r\nS = [a, b, c], T = [1] ;\r\nS = [a, b], T = [1, 2] ;\r\nS = [a, b], T = [1] ;\r\nS = [a, c], T = [1, 2] ;\r\nS = [a, c], T = [1] ;\r\nS = [a], T = [1, 2] ;\r\nS = [a], T = [1] ;\r\nno\r\n\r\n?- S `:: [a] + [b, c], T `:: [1] + [2], set_labeling(S).\r\nS = [a, b, c] ;\r\nS = [a, b] ;\r\nS = [a, c] ;\r\nS = [a] ;\r\nno\r\n\r\n", see_also : [set_labeling / 2, refine / 2]]). :- comment(set_labeling / 2, [amode : set_labeling(++, +), args : ["UpDown" : "Atom: 'up' or 'down'.", "SetVars" : "List of set variables."], summary : "Label set variables", desc : html("Instantiate all variables in SetVars from first to last, with\r\n\t\tconsecutive refinements of their domains until they are ground.
\r\n\t\tIf heuristic UpDown is 'up' then, for each set variable, for each element\r\n\t\tin its poss (lub\\glb), inclusion is tried first; otherwise (down)\r\n\t\texclusion is tried first."), resat : "Yes.", fail_if : "Fails if SetVars can not be labeled (there is no solution to the CSP).", eg : "\r\n?- S `:: [a] + [b, c], T `:: [1] + [2], set_labeling(up, [S, T]).\r\nS = [a, b, c], T = [1, 2] ;\r\nS = [a, b, c], T = [1] ;\r\nS = [a, b], T = [1, 2] ;\r\nS = [a, b], T = [1] ;\r\nS = [a, c], T = [1, 2] ;\r\nS = [a, c], T = [1] ;\r\nS = [a], T = [1, 2] ;\r\nS = [a], T = [1] ;\r\nno\r\n\r\n?- S `:: [a] + [b, c], T `:: [1] + [2], set_labeling(down, [S, T]).\r\nS = [a], T = [1] ;\r\nS = [a], T = [1, 2] ;\r\nS = [a, c], T = [1] ;\r\nS = [a, c], T = [1, 2] ;\r\nS = [a, b], T = [1] ;\r\nS = [a, b], T = [1, 2] ;\r\nS = [a, b, c], T = [1] ;\r\nS = [a, b, c], T = [1, 2] ;\r\nno\r\n", see_also : [set_labeling / 1, refine / 2]]). :- comment(sets / 4, [amode : sets(+, ++, ++, +), args : ["SetVariables" : "A list of variables.", "Glb" : "A ground set.", "Poss" : "A ground set.", "Functions" : "A list."], summary : "Set variables declaration with optional functions", desc : html("Declare or constrain set domain variables to have Glb as assured\r\n\t\telements and Poss as the possible additional elements.
\r\n\t\tFunctions is a list of functions over each SetVariable in SetVariables in the form\r\n\t\tFunctionName:FunctionValue, where FunctionName can be 'cardinality',\r\n\t\t'minimum', 'maximum' or 'union':
\r\n
\r\n cardinality: FunctionValue can be an integer, an FD variable or an integer domain (list or range)\r\n union: (SetVariable must be a set of sets.) FunctionValue can be a set, a set variable\r\n\tor a set domain in the form GlbUnion+PossUnion, representing the glb and poss of\r\n\tthe union of SetVariable\r\n minimum and maximum: (SetVariable must be a nonempty set of integers.)\r\n\tFunctionValue can be an integer, an FD variable or an integer domain\r\n\r\n\t\tCardinal inferences over SetVariable and its union, minimum and maximum\r\n\t\tfunctions will be performed only if these functions are explicitly\r\n\t\tdeclared, whereas the cardinality function and respective inferences\r\n\t\twill always be present even if this (cardinality) function is not\r\n\t\texplicitly declared. Note that a simple function declaration such as\r\n\t\tminimum:_ is sufficient to make it 'active'.
\r\n\t\tIf a FunctionValue is given as a variable or as a fixed (integer or set)\r\n\t\tvalue, then it will be the same for all of SetVariables. If it is given\r\n\t\tas a domain, then function values for SetVariables may be different\r\n\t\t(a different domain variable is created for each SetVariable)."), resat : "No.", fail_if : "Fails if SetVariables can not be constrained accordingly.", eg : "\r\n?- sets([S],[],[a,b],[]).\r\n?- sets([S,T],[],[a,b],[cardinality:1]).\r\n?- sets([X,Y,Z],[],[a,b],[cardinality:C]).\r\n?- sets([X,Y,Z],[],[a,b],[cardinality:[0,2]]).\r\n?- sets([X,Y,Z],[c],[a,b,d,e,f,g,h,i,j,k],[cardinality:[2,4..7]]).\r\n?- sets([X,Y,Z],[],[1,3,4,5,7],[minimum:Min,maximum:1..9]), fd:(Max #> Min+2).\r\n?- sets([X,Y,Z], [], [[1,2,5],[2,4],[3,5],[1,3,4]], [union:[1]+[2,4,5]]).\r\n", see_also : [set / 4, `:: / 2, cardinality / 2, union_var / 2, minimum / 2, maximum / 2, set_labeling / 1]]). :- comment(union_var / 2, [amode : union_var(?, ?), args : ["SetVariable" : "A Set (variable or ground) of sets.", "UnionVar" : "A Set (variable or ground)."], summary : "Union of a set of sets", desc : html("UnionVar is the union of sets in SetVariable. If UnionVar is given\r\n\t\t(as a ground set or a set variable), then SetVariable is constrained to have such union.\r\n\t\tIf UnionVar is a free variable, then it is unified with the set's union as\r\n\t\ta set variable or a ground set (if it is already known).
\r\n\t\tunion_var/2 can thus be used either to declare (or constrain) a union\r\n\t\tfunction or to retrieve it."), resat : "No.", fail_if : "Fails if UnionVar can not be the union of SetVariable.", eg : "\r\n?- S `::[]..[[a],[b]], union_var(S,U).\r\n?- S `::[]..[[a],[b],[a,b]], union_var(S,[a,b]).\r\n?- union_var([[a,b],[b,c]], U).\r\nU = [a,b,c]", see_also : [set / 4, sets / 4, cardinality / 2]]).